i:Id, k:Knd, L:IdLnk List.
@i: k sends only on links in L ||- es.@i:k sends only on links in L 

latex

Definitions	es realizer ind Rbframe compseq tag def, Consistent(R;es), ES, t  T, x:A. B(x), @loc: k sends only on links in L, @i:k sends only on links in L, x:AB(x), P  Q, True, R-Feasible(R), inr(x), x:AB(x), P & Q, R ||- es.P(es), Id, Knd, IdLnk, type List
Lemmas	IdLnk wf, Knd wf, Id wf, R-consistent wf, Rbframe wf, event system wf